Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(map,f),nil)  → nil
2:    app(app(map,f),app(app(cons,x),xs))  → app(app(cons,app(f,x)),app(app(map,f),xs))
3:    app(app(le,0),y)  → true
4:    app(app(le,app(s,x)),0)  → false
5:    app(app(le,app(s,x)),app(s,y))  → app(app(le,x),y)
6:    app(app(maxlist,x),app(app(cons,y),ys))  → app(app(if,app(app(le,x),y)),app(app(maxlist,y),ys))
7:    app(app(maxlist,x),nil)  → x
8:    app(height,app(app(node,x),xs))  → app(s,app(app(maxlist,0),app(app(map,height),xs)))
There are 17 dependency pairs:
9:    APP(app(map,f),app(app(cons,x),xs))  → APP(app(cons,app(f,x)),app(app(map,f),xs))
10:    APP(app(map,f),app(app(cons,x),xs))  → APP(cons,app(f,x))
11:    APP(app(map,f),app(app(cons,x),xs))  → APP(f,x)
12:    APP(app(map,f),app(app(cons,x),xs))  → APP(app(map,f),xs)
13:    APP(app(le,app(s,x)),app(s,y))  → APP(app(le,x),y)
14:    APP(app(le,app(s,x)),app(s,y))  → APP(le,x)
15:    APP(app(maxlist,x),app(app(cons,y),ys))  → APP(app(if,app(app(le,x),y)),app(app(maxlist,y),ys))
16:    APP(app(maxlist,x),app(app(cons,y),ys))  → APP(if,app(app(le,x),y))
17:    APP(app(maxlist,x),app(app(cons,y),ys))  → APP(app(le,x),y)
18:    APP(app(maxlist,x),app(app(cons,y),ys))  → APP(le,x)
19:    APP(app(maxlist,x),app(app(cons,y),ys))  → APP(app(maxlist,y),ys)
20:    APP(app(maxlist,x),app(app(cons,y),ys))  → APP(maxlist,y)
21:    APP(height,app(app(node,x),xs))  → APP(s,app(app(maxlist,0),app(app(map,height),xs)))
22:    APP(height,app(app(node,x),xs))  → APP(app(maxlist,0),app(app(map,height),xs))
23:    APP(height,app(app(node,x),xs))  → APP(maxlist,0)
24:    APP(height,app(app(node,x),xs))  → APP(app(map,height),xs)
25:    APP(height,app(app(node,x),xs))  → APP(map,height)
The approximated dependency graph contains one SCC: {9,11-13,15,17,19,22,24}.
Tyrolean Termination Tool  (5.53 seconds)   ---  May 3, 2006